/LMAR=0/XLINE=4/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#4=FIX20
␈↓ ↓N␈↓α␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α1TABLE OF CONTENTS␈↓ di


␈↓ ↓N␈↓α␈↓ α∞Section␈↓ ¬mPage

␈↓ ↓N␈↓␈↓ ↓n1.1  FORMAL REASONING␈↓ ε  1
␈↓ ↓N␈↓␈↓ α≡1.1.1  The Epistemological Part of
␈↓ ↓N␈↓␈↓ αnArti≡cial Intelligence␈↓ ε  1
␈↓ ↓N␈↓␈↓ α≡1.1.2  Proof Checking␈↓ ε  2
␈↓ ↓N␈↓␈↓ α≡1.1.3  Program Correctness␈↓ ε  3
␈↓ ↓N␈↓␈↓ α≡1.1.4  Common Sense Reasoning␈↓ ε  3
␈↓ ↓N␈↓␈↓ α≡1.1.5  Goals and milestones.␈↓ ε  5
␈↓ ↓N␈↓␈↓ α≡1.1.6  The Formal Reasoning Group.␈↓ ε  6
␈↓ ↓N␈↓α␈↓ b1


␈↓ ↓N␈↓α␈↓ ↓n1.1  FORMAL REASONING                       ␈↓ π∞␈↓methods␈α∪themselves.␈α∪ However,␈α∀it␈α∪eventually
                                            ␈↓ π∞␈↓became␈α∃quite␈α∃clear␈α∃that␈α∃in␈α∃most␈α∃classes␈α∀of
␈↓ ↓N␈↓This␈α'includes␈α'the␈α(activities␈α'previously         ␈↓ π∞␈↓problems␈α⊃the␈α⊃barrier␈α⊃to␈α⊃approaching␈α⊂human
␈↓ ↓N␈↓reported␈α#as␈α$proof-checking,␈α#mathematical       ␈↓ π∞␈↓performance␈α≠lay␈α≠in␈α≠the␈α≤representation␈α≠of
␈↓ ↓N␈↓theory␈α~of␈α~computation,␈α≠and␈α~representation       ␈↓ π∞␈↓information␈α"rather␈α"than␈α"in␈α"the␈α"search
␈↓ ↓N␈↓theory.␈α∂ They␈α∂are␈α∂combined␈α∂in␈α∂this␈α∂proposal,      ␈↓ π∞␈↓methods.␈α Moreover,␈αinformation␈αrelevant␈αto␈αa
␈↓ ↓N␈↓because␈αmuch␈α
the␈αsame␈α
people␈αare␈αinvolved␈α
in       ␈↓ π∞␈↓problem␈αhas␈αto␈αbe␈αtaken␈αin␈αthe␈αform␈αin␈αwhich
␈↓ ↓N␈↓all␈α
of␈αthem,␈α
and␈α
they␈αrequire␈α
some␈α
of␈αthe␈α
same       ␈↓ π∞␈↓it␈α≠can␈α~most␈α≠easily␈α~be␈α≠learned␈α≠and␈α~then
␈↓ ↓N␈↓developments of ideas and of software.      ␈↓ π∞␈↓transformed␈α∃into␈α∃the␈α∃most␈α∃useful␈α∃form␈α∃for
                                            ␈↓ π∞␈↓solving the problem.
␈↓ ↓N␈↓Before␈α∃describing␈α⊗the␈α∃present␈α∃state␈α⊗of␈α∃this
␈↓ ↓N␈↓work␈α∩and␈α⊃what␈α∩is␈α∩planned␈α⊃in␈α∩the␈α∩next␈α⊃two            ␈↓ π∞␈↓Therefore,␈α∩the␈α⊃attention␈α∩of␈α⊃the␈α∩AI␈α∩≡eld␈α⊃has
␈↓ ↓N␈↓years,␈α≥it␈α≥seems␈α≤desirable␈α≥to␈α≥explain␈α≤the          ␈↓ π∞␈↓lately␈α&tended␈α'to␈α&concentrate␈α'on␈α&what
␈↓ ↓N␈↓rationale␈α∂of␈α⊂this␈α∂e≥ort,␈α⊂which␈α∂is␈α⊂perhaps␈α∂the      ␈↓ π∞␈↓information␈α∪an␈α∪intelligent␈α∪system␈α∪needs␈α∩and
␈↓ ↓N␈↓Laboratory's␈α∃major␈α∃e≥ort␈α∃in␈α∃the␈α∀theoretical      ␈↓ π∞␈↓can␈αget␈αfor␈αits␈αwork␈αand␈αhow␈αthis␈αinformation
␈↓ ↓N␈↓side of arti≡cial intelligence.             ␈↓ π∞␈↓is␈α∂to␈α∂be␈α⊂represented␈α∂in␈α∂the␈α∂computer,␈α⊂i.e.␈α∂the
                                            ␈↓ π∞␈↓␈↓↓epistemological␈↓␈αpart␈α
of␈αthe␈α
AI␈αproblem.␈α In␈α
our
␈↓ ↓N␈↓α␈↓ α∞1.1.1  The Epistemological Part of          ␈↓ π∞␈↓analysis,␈αit␈α
is␈αessential␈αto␈α
consider␈α␈↓αnot␈αonly␈↓␈α
the
␈↓ ↓N␈↓α␈↓ αNArti≡cial Intelligence                      ␈↓ π∞␈↓representation␈α↔of␈α↔information␈α↔but␈α↔also␈α↔the
                                            ␈↓ π∞␈↓methods␈α
of␈α
reasoning␈α
whereby␈α
the␈α
solution␈α
to
␈↓ ↓N␈↓Arti≡cial␈α
intelligence␈α
has␈α
proved␈α
to␈α
be,␈α
as␈α
some   ␈↓ π∞␈↓a␈α≤problem␈α≤follows␈α≤from␈α≤the␈α≤facts.␈α≤ The
␈↓ ↓N␈↓people␈α↔expected␈α⊗and␈α↔others␈α⊗didn't,␈α↔a␈α⊗very         ␈↓ π∞␈↓following␈α3still␈α3somewhat␈α3controversial
␈↓ ↓N␈↓di≠cult␈αscienti≡c␈αsubject.␈α In␈αthe␈α≡rst␈αten␈αyears  ␈↓ π∞␈↓principle␈α
underlying␈α
our␈α
work␈α
was␈α∞≡rst␈α
stated
␈↓ ↓N␈↓of␈α⊃AI␈α∩research,␈α⊃the␈α⊃limits␈α∩of␈α⊃what␈α∩could␈α⊃be         ␈↓ π∞␈↓in [McCarthy 1959]:
␈↓ ↓N␈↓done␈α≠by␈α≠straightforward␈α≠programming␈α~on
␈↓ ↓N␈↓speci≡c␈α∀intellectual␈α∃problems␈α∀such␈α∃as␈α∀games      ␈↓ π∞␈↓␈↓α"In␈α∩order␈α⊃for␈α∩a␈α⊃program␈α∩to␈α⊃be␈α∩capable␈α⊃of
␈↓ ↓N␈↓and␈α∞theorem␈α∞proving␈α∞were␈α∞explored.␈α∞ Besides      ␈↓ π∞␈↓αlearning␈α∞something␈α∞it␈α∞must␈α∞≡rst␈α∂be␈α∞capable
␈↓ ↓N␈↓that,␈αa␈α
number␈αof␈α
ideas␈αfor␈α
general␈αintelligent    ␈↓ π∞␈↓αof␈α⊗being␈α∃told␈α⊗it."␈↓␈α⊗The␈α∃test␈α⊗of␈α⊗whether␈α∃a
␈↓ ↓N␈↓systems␈α
were␈αalso␈α
explored␈α
with␈αlimited␈α
results.  ␈↓ π∞␈↓person␈α∪or␈α∪a␈α∪computer␈α∀program␈α∪␈↓↓understands␈↓
␈↓ ↓N␈↓It␈α_became␈α_clear␈α_that␈α_computer␈α→systems␈α_of          ␈↓ π∞␈↓the␈αfacts␈αof␈αa␈αproblem␈αcan␈αbe␈αtested␈αsomewhat
␈↓ ↓N␈↓human␈α
intelligence␈α
level␈α
were␈α
not␈α
going␈α
to␈αbe      ␈↓ π∞␈↓independently␈α∩of␈α∩problem␈α∩solving␈α∪ability␈α∩by
␈↓ ↓N␈↓obtained␈α∀in␈α∀one␈α∀grand␈α∀rush.␈α∀ Once␈α∀this␈α∀is          ␈↓ π∞␈↓testing␈α∞whether␈α∞he␈α∞or␈α∞it␈α∞can␈α∞follow,␈α∞i.e.␈α∞check
␈↓ ↓N␈↓understood,␈α∃it␈α∃becomes␈α∃important␈α∃to␈α∃try␈α∃to        ␈↓ π∞␈↓the␈α∪correctness␈α∪of,the␈α∪reasoning␈α∀involved␈α∪in
␈↓ ↓N␈↓analyze␈α∞the␈α∞arti≡cial␈α∞intelligence␈α∞problem␈α∞into  ␈↓ π∞␈↓the␈α∩solution␈α∩of␈α∩the␈α∩problem.␈α∩ Moreover,␈α⊃the
␈↓ ↓N␈↓a␈αcollection␈αof␈αsubproblems␈αand␈αtry␈αto␈αsplit␈αo≥     ␈↓ π∞␈↓ability␈αto␈α
follow␈αthe␈α
reasoning␈αis␈αa␈α
prerequisite
␈↓ ↓N␈↓subproblems␈α∃that␈α∃can␈α∃be␈α∃tackled␈α∀separately       ␈↓ π∞␈↓to the ability to generate it.
␈↓ ↓N␈↓and␈α↔whose␈α_solution␈α↔will␈α↔contribute␈α_to␈α↔the
␈↓ ↓N␈↓solution␈αof␈αthe␈αproblem␈αas␈αa␈αwhole.␈α One␈αsuch       ␈↓ π∞␈↓However,␈α
when␈α
we␈α
compare␈α
human␈α∞ability␈α
to
␈↓ ↓N␈↓analysis␈α⊂(McCarthy␈α⊂and␈α⊂Hayes␈α⊂1970)␈α∂divides       ␈↓ π∞␈↓follow␈α∂reasoning␈α∂with␈α∂what␈α∂we␈α∂know␈α∂how␈α∂to
␈↓ ↓N␈↓the␈α≡arti≡cial␈α≡intelligence␈α≡problem␈α≡into␈α≡a        ␈↓ π∞␈↓make␈α
machines␈αdo,␈α
we␈αdiscover␈α
that␈αwe␈α
cannot
␈↓ ↓N␈↓␈↓↓heuristic␈↓ part and an ␈↓↓epistemological␈↓ part. ␈↓ π∞␈↓yet␈α≥make␈α≤them␈α≥even␈α≤follow␈α≥the␈α≤human
                                            ␈↓ π∞␈↓reasoning␈α≤involved␈α≤in␈α≤solving␈α≤such␈α≠very
␈↓ ↓N␈↓The␈α␈↓↓heuristic␈↓␈αpart␈αof␈αthe␈αproblem␈α
was␈αtackled      ␈↓ π∞␈↓simple␈α
real␈α
life␈α
problems␈α
as␈α
how␈α
to␈α
travel␈α
from
␈↓ ↓N␈↓≡rst␈α↔and␈α⊗is␈α↔best␈α⊗understood.␈α↔ It␈α⊗essentially      ␈↓ π∞␈↓my␈α∂home␈α∞to␈α∂the␈α∞ARPA␈α∂o≠ce␈α∂in␈α∞Washington
␈↓ ↓N␈↓involves␈α≤methods␈α≤of␈α≤searching␈α≥spaces␈α≤of          ␈↓ π∞␈↓or␈α∞even␈α∞the␈α∞reasoning␈α∞involved␈α∞in␈α∞the␈α
proofs
␈↓ ↓N␈↓possibilities␈α⊗for␈α⊗the␈α∃solution␈α⊗to␈α⊗a␈α∃problem.      ␈↓ π∞␈↓of␈α
mathematical␈α
theorems.␈α
 This␈α
lack␈αof␈α
ability
␈↓ ↓N␈↓The␈α~tendency␈α~of␈α~this␈α~work␈α~was␈α~to␈α→take              ␈↓ π∞␈↓has two aspects:
␈↓ ↓N␈↓whatever␈α
came␈α
easily␈α
to␈α
hand␈α
as␈α
the␈α∞space␈α
of
␈↓ ↓N␈↓possibilities␈α↔and␈α↔concentrate␈α↔on␈α↔the␈α⊗search      ␈↓ π∞␈↓First,␈α
we␈α
cannot␈αyet␈α
formally␈α
express␈α
the␈αfacts
␈↓ ↓:␈↓α2␈↓ Z


␈↓ ↓:␈↓we␈α∪know␈α∪about␈α∀how␈α∪the␈α∪world␈α∀works,␈α∪and             ␈↓ εz␈↓propositions.␈α∩ it␈α∩is␈α⊃very␈α∩important␈α∩to␈α⊃reduce
␈↓ ↓:␈↓second␈α→even␈α→when␈α→the␈α→facts␈α→are␈α_formally           ␈↓ εz␈↓this,␈α∀because␈α∃when␈α∀we␈α∃later␈α∀want␈α∃to␈α∀make
␈↓ ↓:␈↓expressable,␈αas␈α
in␈αthe␈α
case␈αof␈α
mathematics,␈αwe     ␈↓ εz␈↓computer␈α≤programs␈α≠capable␈α≤of␈α≠generating
␈↓ ↓:␈↓still␈α∪haven't␈α∪been␈α∪quite␈α∪able␈α∪to␈α∪express␈α∩the       ␈↓ εz␈↓these␈α~proofs,␈α~the␈α≠ideas␈α~that␈α~have␈α≠to␈α~be
␈↓ ↓:␈↓informal␈αreasoning␈αin␈αa␈αformal␈α
way␈αcheckable      ␈↓ εz␈↓generated␈α_will␈α↔correspond␈α_in␈α_a␈α↔substantial
␈↓ ↓:␈↓by machine.                                 ␈↓ εz␈↓degree␈α∞to␈α∞the␈α∞proof␈α∞steps,␈α∞and␈α∞the␈α∞amount␈α∞of
                                            ␈↓ εz␈↓work␈α→will␈α_tend␈α→to␈α_be␈α→exponential␈α→in␈α_the
␈↓ ↓:␈↓The␈α∀␈↓αFormal␈α∪Reasoning␈α∀Group␈↓␈α∀is␈α∪pursuing           ␈↓ εz␈↓number of steps.
␈↓ ↓:␈↓both␈α⊃problems.␈α⊃ The␈α⊃easier␈α⊃problem,␈α⊃though
␈↓ ↓:␈↓still␈αquite␈αdi≠cult,␈αseems␈αto␈αbe␈αexpressing,␈αin␈α
a   ␈↓ εz␈↓The␈α∪reason␈α∪for␈α∩putting␈α∪a␈α∪major␈α∪e≥ort␈α∩into
␈↓ ↓:␈↓completely␈αformal␈αand␈αmachine-checkable␈αway,    ␈↓ εz␈↓checking␈α⊃proofs␈α⊃in␈α⊂pure␈α⊃mathematics␈α⊃is␈α⊂that
␈↓ ↓:␈↓the␈α3reasoning␈α3involved␈α3in␈α2proving               ␈↓ εz␈↓pure␈αmathematics␈αprovides␈αthe␈α
most␈αextensive
␈↓ ↓:␈↓mathematical␈αtheorems.␈α The␈αproblem␈αis␈αto␈α
get     ␈↓ εz␈↓example␈α∂of␈α∂long␈α∂chains␈α∂of␈α⊂human␈α∂reasoning,
␈↓ ↓:␈↓the␈α∪basic␈α∩mathematical␈α∪knowledge␈α∩expressed      ␈↓ εz␈↓and␈α∨moreover␈α∨the␈α∨problem␈α∨of␈α≡checking
␈↓ ↓:␈↓in␈αreally␈αuseable␈αaxioms␈αand␈αalso␈α
to␈αformalize     ␈↓ εz␈↓mathematical␈α∪reasoning␈α∪is␈α∀uncomplicated␈α∪by
␈↓ ↓:␈↓enough␈α⊂of␈α∂the␈α⊂metamathematics␈α∂to␈α⊂deal␈α∂with        ␈↓ εz␈↓di≠culties␈α∂in␈α∞axiomatizing␈α∂the␈α∂subject␈α∞matter
␈↓ ↓:␈↓the␈α≠fact␈α≠that␈α≠much␈α≠of␈α≠the␈α≠reasoning␈α≠is             ␈↓ εz␈↓correctly␈α≡even␈α≡though␈α≡there␈α≡still␈α≥remain
␈↓ ↓:␈↓metamathematical;␈α∪i.e.␈α∀instead␈α∪of␈α∀giving␈α∪the     ␈↓ εz␈↓di≠culties␈α∩in␈α∩axiomatizing␈α∩it␈α∩in␈α∩a␈α∩way␈α⊃that
␈↓ ↓:␈↓proof␈α∂from␈α∂the␈α∂axioms,␈α∂mathematicians␈α∞often      ␈↓ εz␈↓corresponds closely to our intuitive ideas.
␈↓ ↓:␈↓reason␈α
informally␈α
about␈α
the␈α
axioms␈α
and␈α
rules
␈↓ ↓:␈↓of␈α∀inference␈α∀and␈α∀show␈α∀that␈α∀a␈α∀proof␈α∪exists.         ␈↓ εz␈↓There␈α∃is␈α∃some␈α∃controversy␈α∃in␈α∃the␈α∃AI␈α∃≡eld
␈↓ ↓:␈↓This␈α∂is␈α∂just␈α∂as␈α∂convincing␈α∂as␈α∂a␈α∂proof␈α∞within        ␈↓ εz␈↓about␈α∂the␈α∂appropriateness␈α∂of␈α∂≡rst␈α⊂order␈α∂logic
␈↓ ↓:␈↓the␈α∩theory␈α⊃and␈α∩is␈α⊃often␈α∩much␈α∩more␈α⊃concise.         ␈↓ εz␈↓for␈αexpressing␈αa␈α
program␈αneeds␈αto␈α
know.␈α We
␈↓ ↓:␈↓However,␈αit␈αusually␈αdepends␈αon␈αconsiderations    ␈↓ εz␈↓will␈α∪not␈α∪discuss␈α∪what␈α∪various␈α∪authors␈α∪have
␈↓ ↓:␈↓that␈α⊃are␈α⊃often␈α⊃not␈α⊃formalized;␈α⊃moreover,␈α⊂the      ␈↓ εz␈↓said␈αhere,␈αbut␈αwe␈αwill␈αexplain␈αthe␈αbasis␈αof␈αour
␈↓ ↓:␈↓switches␈α∂between␈α∞reasoning␈α∂within␈α∂the␈α∞theory     ␈↓ εz␈↓continued␈α∃reliance␈α∃on␈α∃logic␈α∃and␈α⊗≡rst␈α∃order
␈↓ ↓:␈↓and␈α,reasoning␈α-about␈α,it␈α-are␈α,usualy                ␈↓ εz␈↓logic␈αin␈αparticular.␈α First,␈αwe␈αwill␈αanswer␈αthose
␈↓ ↓:␈↓unannounced.␈α⊂ We␈α⊃need␈α⊂to␈α⊃be␈α⊂able␈α⊃to␈α⊂make           ␈↓ εz␈↓who␈α⊃say␈α⊃that␈α⊃a␈α⊃procedural␈α⊃representation␈α⊃of
␈↓ ↓:␈↓our␈α⊂programs␈α∂accept␈α⊂and␈α⊂eventually␈α∂generate      ␈↓ εz␈↓information␈α∞is␈α
always␈α∞preferable.␈α
 ␈↓↓Information
␈↓ ↓:␈↓this␈α_kind␈α→of␈α_reasoning,␈α_and␈α→this␈α_requires         ␈↓ εz␈↓↓obtained␈α⊂from␈α⊂observation␈α⊂or␈α⊃communication␈α⊂is
␈↓ ↓:␈↓formalizing␈α
the␈α
metamathematics␈α
in␈α
a␈α
practical   ␈↓ εz␈↓↓not␈α⊂usually␈α⊂received␈α⊂in␈α⊂procedural␈α⊃form.␈α⊂ The
␈↓ ↓:␈↓way.                                        ␈↓ εz␈↓↓process␈αof␈αtransforming␈α
it␈αto␈αprocedural␈αform␈α
is
                                            ␈↓ εz␈↓↓the␈α⊃subject␈α⊃matter␈α⊃of␈α∩automatic␈α⊃programming.
␈↓ ↓:␈↓α␈↓ ↓z1.1.2  Proof Checking                       ␈↓ εz␈↓↓Second,␈α∀no␈α∀procedural␈α∀form␈α∀so␈α∀far␈α∀proposed
                                            ␈↓ εz␈↓↓provides␈α∀for␈α∀following␈α∀reasoning␈α∀or␈α∀provides
␈↓ ↓:␈↓We␈α⊂now␈α⊂have␈α∂a␈α⊂proof-checking␈α⊂program␈α∂for          ␈↓ εz␈↓↓rules␈α→that␈α_determine␈α→when␈α_a␈α→conclusion␈α_is
␈↓ ↓:␈↓≡rst␈α
order␈α∞logic␈α
which,␈α
after␈α∞several␈α
revisions,  ␈↓ εz␈↓↓correctly␈α$drawn.␈α% Third,␈α$we␈α%agree␈α$that
␈↓ ↓:␈↓seems␈α
good␈α∞enough␈α
to␈α∞accept␈α
proofs␈α∞of␈α
actual       ␈↓ εz␈↓↓procedural␈αknowledge␈αis␈αimportant␈αand␈αmust␈α
be
␈↓ ↓:␈↓mathematical␈α
theorems␈α
of␈αsubstantial␈α
di≠culty.  ␈↓ εz␈↓↓provided␈α∨in␈α intelligent␈α∨systems,␈α but␈α∨also
␈↓ ↓:␈↓In␈α∞the␈α∞next␈α∞two␈α∞years␈α∞we␈α∞shall␈α∞verify␈α∞this␈α∞by        ␈↓ εz␈↓↓declarative␈α∨knowledge␈α≡about␈α∨procedures␈α≡is
␈↓ ↓:␈↓checking␈αthe␈α
proofs␈αof␈α
well-known␈αtheorems␈α
in     ␈↓ εz␈↓↓important.␈↓
␈↓ ↓:␈↓combinatorics␈α∩and␈α∪set␈α∩theory.␈α∪ In␈α∩particular,
␈↓ ↓:␈↓we␈αhope␈αto␈α
formalize␈αthe␈αreasoning␈αin␈α
Cohen's      ␈↓ εz␈↓We␈αare␈αnot␈α
asserting␈αthat␈αif␈α
only␈αthe␈αfacts␈αof␈α
a
␈↓ ↓:␈↓book␈α'␈↓↓Set␈α'Theory␈α'and␈α'the␈α'Continuum                ␈↓ εz␈↓situation␈α∩can␈α∩be␈α∩all␈α∩expressed␈α∩in␈α∩≡rst␈α∩order
␈↓ ↓:␈↓↓Hypothesis␈↓,␈α
[Cohen␈α
1965],␈α
which␈α
has␈α
a␈αmajor       ␈↓ εz␈↓logic,␈α∩a␈α∩general-purpose␈α∩≡rst␈α∪order␈α∩problems
␈↓ ↓:␈↓metamathematical␈α∪component.␈α∪ In␈α∀the␈α∪initial     ␈↓ εz␈↓solver␈αwill␈αbe␈αintelligent.␈α The␈αproblem␈αsolvers
␈↓ ↓:␈↓versions␈α∂of␈α∂computer␈α∂proof␈α∂checkers,␈α⊂it␈α∂turns     ␈↓ εz␈↓will␈α≡need␈α∨special␈α≡features␈α∨for␈α≡particular
␈↓ ↓:␈↓out␈αthat␈αthe␈αproofs␈αare␈αvery␈αmuch␈αlonger␈αthan       ␈↓ εz␈↓searches,␈α⊃and␈α∩we␈α⊃expect␈α∩that␈α⊃many␈α∩of␈α⊃these
␈↓ ↓:␈↓the␈α≡usual␈α≡informal␈α≡proofs␈α≡of␈α≡the␈α≥same             ␈↓ εz␈↓features␈α~will␈α~come␈α~from␈α→metamathematical
␈↓ ↓N␈↓α1.1  FORMAL REASONING␈↓ `3


␈↓ ↓N␈↓logical␈α∪reasoning␈α∪carried␈α∩out␈α∪by␈α∪the␈α∩system.      ␈↓ π∞␈↓computer␈α∞programs.␈α∞ The␈α∞reasons␈α∞why␈α∞this␈α∞is
␈↓ ↓N␈↓Intelligent␈αsystems␈α
will␈αalso␈α
use␈αother␈α
kinds␈αof   ␈↓ π∞␈↓so␈α∃were␈α∃elaborated␈α∃in␈α∃some␈α∃of␈α⊗our␈α∃earlier
␈↓ ↓N␈↓data␈α≤than␈α≤sentences,␈α≤and␈α≥the␈α≤attachment          ␈↓ π∞␈↓proposals␈α~to␈α~ARPA␈α~[Stanford␈α~1969],␈α→and
␈↓ ↓N␈↓feature of FOL already provides for this.   ␈↓ π∞␈↓pursuing␈α⊂this␈α⊂approach␈α∂has␈α⊂been␈α⊂one␈α⊂of␈α∂the
                                            ␈↓ π∞␈↓major␈α⊃tasks␈α∩of␈α⊃our␈α⊃ARPA␈α∩contract.␈α⊃ ␈↓↓Second␈↓,
␈↓ ↓N␈↓There␈α→are␈α_also␈α→those␈α_who␈α→like␈α→logic␈α_but            ␈↓ π∞␈↓this␈α∃domain␈α∃complements␈α∃pure␈α∀mathematics
␈↓ ↓N␈↓consider␈α'≡rst␈α&order␈α'logic␈α'too␈α&limited.           ␈↓ π∞␈↓nicely␈α∀as␈α∪a␈α∀test␈α∀of␈α∪our␈α∀ability␈α∀to␈α∪formalize
␈↓ ↓N␈↓Sometimes␈α∂they␈α∂have␈α⊂in␈α∂mind␈α∂the␈α⊂≡rst␈α∂order         ␈↓ π∞␈↓reasoning,␈α⊂because␈α⊂there␈α⊂is␈α⊂still␈α⊃a␈α⊂substantial
␈↓ ↓N␈↓algebraic␈α$theories␈α$that␈α$have␈α$played␈α#a            ␈↓ π∞␈↓conceptual␈α⊃problem␈α⊂of␈α⊃determining␈α⊃what␈α⊂the
␈↓ ↓N␈↓signi≡cant␈α_role␈α_in␈α_the␈α_metamathematics␈α↔of        ␈↓ π∞␈↓right␈α∃axioms␈α∃are.␈α∃ ␈↓↓Third␈↓,␈α∃AI␈α∃in␈α∃general␈α∃is
␈↓ ↓N␈↓algebra␈α∞in␈α∞which␈α∞all␈α∞individuals␈α∞are␈α∞elements     ␈↓ π∞␈↓concerned␈α∂with␈α∂reasoning␈α∂that␈α∂a␈α∂strategy␈α∞will
␈↓ ↓N␈↓of␈α
the␈α
algebra.␈α
 The␈α
reason␈α
for␈α
accepting␈αthis     ␈↓ π∞␈↓solve␈α∞a␈α∞problem,␈α∞and␈α∞strategies␈α∞are␈α∞a␈α∞kind␈α
of
␈↓ ↓N␈↓limitation␈α∩in␈α∩the␈α∩mathematical␈α∩study␈α∩is␈α∩that      ␈↓ π∞␈↓program.␈α≡ Therefore,␈α≡the␈α∨mathematics␈α≡of
␈↓ ↓N␈↓the␈α∞compactness␈α∞properties␈α∞of␈α∞≡rst␈α∞order␈α
logic    ␈↓ π∞␈↓program␈α≠correctness␈α≠is␈α≠likely␈α≠to␈α≤play␈α≠an
␈↓ ↓N␈↓have␈α⊗interesting␈α⊗consequences␈α↔for␈α⊗algebraic     ␈↓ π∞␈↓essential␈α↔role␈α_in␈α↔arti≡cial␈α↔intelligence␈α_as␈α↔a
␈↓ ↓N␈↓concepts␈α≤that␈α≤can␈α≤be␈α≤formalized␈α≤in␈α≠this           ␈↓ π∞␈↓whole.
␈↓ ↓N␈↓restricted␈αway.␈α Since␈αour␈αgoal␈αis␈αa␈αsystem␈αthat
␈↓ ↓N␈↓has␈α∨all␈α∨the␈α∨power␈α∨of␈α informal␈α∨human               ␈↓ π∞␈↓α␈↓ πN1.1.4  Common Sense Reasoning
␈↓ ↓N␈↓reasoning,␈αwe␈αuse␈αset␈αtheory␈αformalized␈αin␈α≡rst
␈↓ ↓N␈↓order␈α⊃logic␈α⊂for␈α⊃almost␈α⊃all␈α⊂our␈α⊃work,␈α⊃and␈α⊂set        ␈↓ π∞␈↓The␈α∂problem␈α∂of␈α∂making␈α∂computers␈α∂carry␈α∂out
␈↓ ↓N␈↓theory␈α∩is␈α∩as␈α∩powerful␈α∩as␈α∩any␈α∩of␈α∩the␈α∩higher          ␈↓ π∞␈↓common␈α∀sense␈α∀reasoning␈α∀was␈α∀≡rst␈α∀posed␈α∪in
␈↓ ↓N␈↓order␈α_logics␈α_for␈α_all␈α_the␈α_problems␈α→we␈α_are           ␈↓ π∞␈↓[McCarthy␈α≤1959],␈α≤and␈α≤some␈α≤results␈α≠were
␈↓ ↓N␈↓considering.␈α~ Another␈α~technical␈α≠reason␈α~for      ␈↓ π∞␈↓reported␈α⊗in␈α⊗that␈α⊗paper␈α⊗and␈α↔in␈α⊗[McCarthy
␈↓ ↓N␈↓using␈α≡rst␈α
order␈αlogic␈αis␈α
that␈αthe␈α
higher␈αorder     ␈↓ π∞␈↓1963]␈α≥and␈α≥[McCarthy␈α≥and␈α≥Hayes␈α≥1970].
␈↓ ↓N␈↓logics␈α∪are␈α∪incomplete,␈α∪and␈α∪we␈α∀would␈α∪rather        ␈↓ π∞␈↓␈↓αBecause␈α→the␈α→common␈α→sense␈α→problem␈α→has
␈↓ ↓N␈↓have␈α~the␈α→necessary␈α~incompleteness␈α~of␈α→our         ␈↓ π∞␈↓αproved␈αvery␈αdi≠cult␈α
and␈αis␈αvital␈αfor␈α
arti≡cial
␈↓ ↓N␈↓theories␈α≡embodied␈α≡in␈α≡incomplete␈α≡sets␈α≡of          ␈↓ π∞␈↓αintelligence,␈αit␈αis␈αimportant␈αto␈αtry␈αto␈αsplit␈αit
␈↓ ↓N␈↓axioms␈α∪which␈α∪can␈α∪be␈α∪extended␈α∪if␈α∪desirable         ␈↓ π∞␈↓αinto␈α≤subproblems␈α≥that␈α≤can␈α≥be␈α≤attacked
␈↓ ↓N␈↓rather␈αthan␈αembodied␈αin␈αthe␈αlogic␈αitself␈αwhich     ␈↓ π∞␈↓αseparately␈↓.␈α⊂ We␈α⊃have␈α⊂already␈α⊃mentioned␈α⊂the
␈↓ ↓N␈↓might␈α∂have␈α∂to␈α∞be␈α∂rebuilt␈α∂completely␈α∂in␈α∞order       ␈↓ π∞␈↓split␈α⊂into␈α⊃heuristic␈α⊂and␈α⊃epistemological␈α⊂parts.
␈↓ ↓N␈↓to extend it.                               ␈↓ π∞␈↓Now␈αit␈αturns␈α
out␈αthat␈αthe␈α
epistemological␈αpart
                                            ␈↓ π∞␈↓can␈α⊂be␈α⊂further␈α∂split␈α⊂into␈α⊂the␈α⊂subproblems␈α∂of
␈↓ ↓N␈↓Much␈α→more␈α→can␈α→be␈α→said␈α→about␈α→all␈α_these              ␈↓ π∞␈↓discovering␈α∃the␈α∃facts␈α∃of␈α∃the␈α∃common␈α∀sense
␈↓ ↓N␈↓controversial␈α
matters,␈αbut␈α
this␈αis␈α
not␈α
the␈αplace   ␈↓ π∞␈↓world␈α~and␈α~the␈α~problem␈α~of␈α~following,␈α→i.e.
␈↓ ↓N␈↓for␈αit.␈α In␈αour␈αopinion,␈αthe␈αvarious␈αapproaches    ␈↓ π∞␈↓checking, common sense reasoning.
␈↓ ↓N␈↓to␈α&representation␈α&will␈α&eventually␈α%prove
␈↓ ↓N␈↓complementary.                              ␈↓ π∞␈↓Our␈α∀last␈α∀publication␈α∀on␈α∀the␈α∃common␈α∀sense
                                            ␈↓ π∞␈↓facts␈αis␈α[McCarthy␈α
and␈αHayes␈α1970],␈αand␈α
since
␈↓ ↓N␈↓α␈↓ α∞1.1.3  Program Correctness                  ␈↓ π∞␈↓that␈α!time␈α"additional␈α!results␈α"have␈α!been
                                            ␈↓ π∞␈↓obtained␈α∩on␈α∩how␈α∩to␈α∩express␈α∩knowledge␈α∩and
␈↓ ↓N␈↓The␈α∂second␈α∂area␈α⊂in␈α∂which␈α∂we␈α∂want␈α⊂to␈α∂make            ␈↓ π∞␈↓the␈α∂problem␈α∂of␈α∂simultaneous␈α∂action,␈α∂but␈α⊂it␈α∂is
␈↓ ↓N␈↓formal␈α⊃proofs␈α⊃is␈α⊂the␈α⊃correctness␈α⊃of␈α⊂computer      ␈↓ π∞␈↓not␈αquite␈αtime␈αto␈αredo␈αthe␈αwhole␈αformalism␈αof
␈↓ ↓N␈↓programs.␈α⊃ There␈α⊃are␈α⊃three␈α⊃reasons␈α⊃for␈α⊃this:      ␈↓ π∞␈↓that paper.
␈↓ ↓N␈↓␈↓↓First␈↓,␈α∩verifying␈α∩that␈α∩computer␈α∩programs␈α⊃are
␈↓ ↓N␈↓correct␈α∀by␈α∀proving␈α∀formally␈α∀that␈α∀they␈α∪meet        ␈↓ π∞␈↓We␈α→can␈α→isolate␈α→the␈α→problem␈α→of␈α_following
␈↓ ↓N␈↓their␈αspeci≡cations␈αand␈αchecking␈αthe␈αproofs␈αby    ␈↓ π∞␈↓common␈α
sense␈α
reasoning␈α
from␈α
the␈α
problem␈α
of
␈↓ ↓N␈↓computer␈α is,␈α∨in␈α our␈α∨opinion,␈α the␈α∨most             ␈↓ π∞␈↓≡nding␈α~the␈α→basic␈α~common␈α→sense␈α~facts␈α→by
␈↓ ↓N␈↓promising␈α
practical␈α
technique␈α
in␈α
the␈α
long␈α
run     ␈↓ π∞␈↓≡nding␈αa␈αdomain␈α
in␈αwhich␈αthe␈αfacts␈α
are␈αclear,
␈↓ ↓N␈↓for␈α∞reducing␈α∞the␈α∞time␈α∞necessary␈α∞to␈α∂get␈α∞correct     ␈↓ π∞␈↓but␈α_the␈α↔reasoning␈α_is␈α↔closer␈α_to␈α_real␈α↔world
␈↓ ↓:␈↓α4␈↓ Z


␈↓ ↓:␈↓common␈αsense␈αreasoning␈αthan␈αto␈αmathematical      ␈↓ εz␈↓rigorously,␈α∂but␈α∂the␈α∞reasoning␈α∂involved␈α∂in␈α∞the
␈↓ ↓:␈↓reasoning.␈α∃ Such␈α∃a␈α∀domain␈α∃is␈α∃provided␈α∀by          ␈↓ εz␈↓human␈α∂solution␈α∞of␈α∂certain␈α∞problems␈α∂gives␈α∞up
␈↓ ↓:␈↓certain␈α→chess␈α→problems␈α_in␈α→which␈α→the␈α_tree          ␈↓ εz␈↓using␈α⊂this␈α⊂fact␈α⊂in␈α⊂order␈α⊂to␈α⊂replace␈α⊂reasoning
␈↓ ↓:␈↓search␈α⊂traditional␈α⊃in␈α⊂chess␈α⊃programming␈α⊂has      ␈↓ εz␈↓about␈α∩individual␈α∪moves␈α∩by␈α∪reasoning␈α∩about
␈↓ ↓:␈↓to␈α
be␈α
combined␈α
with␈α
the␈α
step-by-step␈α
deductive    ␈↓ εz␈↓whole␈α∞sequences␈α∞of␈α∞moves.␈α∞ For␈α∞example,␈α∞one
␈↓ ↓:␈↓reasoning␈α∞characteristic␈α
of␈α∞mathematical␈α
logic, ␈↓ εz␈↓problem␈α⊗involves␈α⊗deciding␈α⊗that␈α⊗White␈α∃will
␈↓ ↓:␈↓and␈αboth␈αhave␈αto␈αbe␈αsupplemented␈αby␈αa␈αmode          ␈↓ εz␈↓move␈αhis␈αking␈αalong␈αa␈αcertain␈αpath␈αand␈αattack
␈↓ ↓:␈↓that␈α∞corresponds␈α
to␈α∞observing␈α∞the␈α
chessboard.    ␈↓ εz␈↓a␈α≡certain␈α≡pawn␈α≡of␈α≡the␈α≡opponent.␈α≡ The
␈↓ ↓:␈↓This␈α(mode␈α(combines␈α)observation␈α(and              ␈↓ εz␈↓reasoning␈α∪that␈α∩this␈α∪attack␈α∩will␈α∪be␈α∩successful
␈↓ ↓:␈↓computation␈α∀in␈α∀a␈α∪way␈α∀that␈α∀is␈α∀not␈α∪properly          ␈↓ εz␈↓does␈α∩not␈α∩require␈α∩a␈α∩complete␈α∩analysis␈α∩of␈α∩the
␈↓ ↓:␈↓modeled␈α≥by␈α≥the␈α≥application␈α≥of␈α≥rules␈α≥of            ␈↓ εz␈↓tree␈α∀of␈α∀moves␈α∀that␈α∀Black␈α∀may␈α∃make␈α∀while
␈↓ ↓:␈↓inference.                                  ␈↓ εz␈↓White␈α∩is␈α∪doing␈α∩this.␈α∩ All␈α∪we␈α∩need␈α∪to␈α∩know
                                            ␈↓ εz␈↓about␈αBlack␈α
is␈αwhether␈αhis␈α
king␈αstays␈αwithin␈α
a
␈↓ ↓:␈↓Suppose,␈α∞for␈α∞example,␈α∞the␈α∞solution␈α∞to␈α∂a␈α∞chess      ␈↓ εz␈↓certain␈α"block␈α"of␈α"squares.␈α" The␈α"human
␈↓ ↓:␈↓problem␈α⊗involves␈α⊗the␈α⊗observation␈α⊗that␈α∃one        ␈↓ εz␈↓reasoning␈αsays␈αthat␈αif␈α
he␈αdoes,␈αWhite␈αwins␈α
one
␈↓ ↓:␈↓side␈α⊃is␈α⊂in␈α⊃check␈α⊂in␈α⊃a␈α⊂certain␈α⊃situation.␈α⊂ The       ␈↓ εz␈↓way,␈α∞while␈α∂if␈α∞he␈α∂doesn't,␈α∞White␈α∂wins␈α∞another
␈↓ ↓:␈↓human␈α∪reasoning␈α∀does␈α∪not␈α∪correspond␈α∀to␈α∪a          ␈↓ εz␈↓way.␈α⊃ The␈α⊃reasoning␈α⊂about␈α⊃what␈α⊃happens␈α⊂if
␈↓ ↓:␈↓proof␈α⊂that␈α⊂the␈α⊂side␈α⊂is␈α⊂in␈α⊂check␈α⊂from␈α∂axioms         ␈↓ εz␈↓Black␈α↔leaves␈α_the␈α↔block␈α↔of␈α_squares␈α↔doesn't
␈↓ ↓:␈↓giving␈α∞the␈α∞positions␈α
of␈α∞all␈α∞the␈α∞pieces.␈α
 Rather    ␈↓ εz␈↓depend␈α⊃on␈α⊃how␈α⊃far␈α⊃White␈α⊃has␈α⊃gotten␈α⊂along
␈↓ ↓:␈↓it␈αis␈αa␈αdirect␈αobservation␈αfrom␈αthe␈αboard.␈α On      ␈↓ εz␈↓the␈α∪path␈α∪his␈α∪king␈α∪is␈α∪following␈α∪when␈α∪Black
␈↓ ↓:␈↓the␈α
other␈αhand,␈α
a␈αlot␈α
of␈αthe␈α
human␈αreasoning        ␈↓ εz␈↓makes␈αhis␈αfatal␈αmove.␈α Of␈αcourse,␈αin␈αprinciple,
␈↓ ↓:␈↓in␈α∃chess␈α∀and␈α∃common␈α∀sense␈α∃problems␈α∀does           ␈↓ εz␈↓this␈α~logically␈α~complex␈α~but␈α~computationally
␈↓ ↓:␈↓have␈αthe␈αrule-of-inference␈αcharacter.␈α
 The␈αtwo   ␈↓ εz␈↓simple␈αanalysis␈αcould␈αbe␈αreplaced␈αby␈αfollowing
␈↓ ↓:␈↓modes␈α∩of␈α∪reasoning␈α∩are␈α∩nicely␈α∪combined␈α∩by         ␈↓ εz␈↓the␈α
joint␈αmove␈α
tree␈αof␈α
the␈αtwo␈α
players,␈αbut␈α
this
␈↓ ↓:␈↓introducing␈α∂a␈α∞correspondence␈α∂between␈α∞certain    ␈↓ εz␈↓isn't␈α∞how␈α
humans␈α∞solve␈α
the␈α∞problem,␈α∞and␈α
the
␈↓ ↓:␈↓predicate␈α∩and␈α∪function␈α∩symbols␈α∩in␈α∪the␈α∩logic       ␈↓ εz␈↓resulting␈α_tree␈α_might␈α_well␈α_be␈α_too␈α→large␈α_to
␈↓ ↓:␈↓and␈α∩certain␈α∩computable␈α∩LISP␈α∩functions␈α∩and        ␈↓ εz␈↓explore.␈α↔ This␈α↔problem␈α↔and␈α↔others␈α_like␈α↔it
␈↓ ↓:␈↓predicates.␈α When␈α
a␈αstatement␈α
involving␈αthese    ␈↓ εz␈↓provide␈α∂an␈α∞entry␈α∂to␈α∞the␈α∂concepts␈α∂involved␈α∞in
␈↓ ↓:␈↓function␈α⊂symbols␈α⊂applied␈α⊂to␈α⊂known␈α∂constants      ␈↓ εz␈↓parallel␈α≤action␈α≤in␈α≤human␈α≥situtations,␈α≤e.g.
␈↓ ↓:␈↓occurs,␈α∞it␈α
can␈α∞be␈α
veri≡ed␈α∞by␈α∞direct␈α
calculation    ␈↓ εz␈↓situations␈α
in␈αwhich␈α
there␈α
are␈αseveral␈α
adversary
␈↓ ↓:␈↓using␈α⊃the␈α∩corresponding␈α⊃LISP␈α∩functions.␈α⊃ In      ␈↓ εz␈↓groups␈α∩and␈α∩natural␈α∩events.␈α∩ Thus␈α∪the␈α∩chess
␈↓ ↓:␈↓the␈α
case␈α
of␈α
chess,␈α
we␈α
call␈α
the␈α
collection␈αof␈α
LISP    ␈↓ εz␈↓problem␈α∂allows␈α⊂us␈α∂to␈α⊂face␈α∂the␈α⊂parallel␈α∂action
␈↓ ↓:␈↓functions␈α∀␈↓↓the␈α∀chess␈α∀eye␈↓.␈α∀ We␈α∀have␈α∪explored        ␈↓ εz␈↓problem␈αin␈α
a␈αsimple␈αform,␈α
where␈αit␈α
is␈αdi≠cult
␈↓ ↓:␈↓what␈α⊂these␈α⊂functions␈α⊂are,␈α⊂but␈α⊂we␈α⊃don't␈α⊂have        ␈↓ εz␈↓enough,␈αuncomplicated␈αby␈αour␈αinability␈αin␈αreal
␈↓ ↓:␈↓anything␈αlike␈αa␈α
complete␈αcollection␈αyet,␈α
because  ␈↓ εz␈↓life␈αsituations␈αto␈αfully␈αspecify␈αwhat␈α
actions␈αare
␈↓ ↓:␈↓even␈α⊂the␈α∂domains␈α⊂that␈α∂these␈α⊂functions␈α∂ought       ␈↓ εz␈↓available␈αto␈α
the␈αactors␈αand␈α
what␈αthe␈α
e≥ects␈αof
␈↓ ↓:␈↓to␈α
have␈α
is␈α
unclear.␈α
 For␈α
example,␈α
some␈α
of␈α
them      ␈↓ εz␈↓their actions may be.
␈↓ ↓:␈↓give␈α≤answers␈α≤when␈α≤the␈α≤position␈α≥is␈α≤only
␈↓ ↓:␈↓partially␈α!speci≡ed,␈α and␈α!this␈α!property␈α is         ␈↓ εz␈↓To␈α∀avoid␈α∀misunderstanding,␈α∀we␈α∃should␈α∀say
␈↓ ↓:␈↓essential␈α∂to␈α∂their␈α∂use.␈α∂ Therefore,␈α∂we␈α⊂need␈α∂to     ␈↓ εz␈↓that␈αthis␈αactivity␈αdoes␈αnot␈αinvolve␈α
writing␈αany
␈↓ ↓:␈↓work␈α~with␈α~some␈α~useful␈α~class␈α≠of␈α~partially          ␈↓ εz␈↓kind␈αof␈αprogram␈αfor␈αplaying␈αchess,␈αbecause␈αwe
␈↓ ↓:␈↓speci≡ed positions.                         ␈↓ εz␈↓are␈α∩here␈α∩studying␈α∩the␈α∪epistemological␈α∩rather
                                            ␈↓ εz␈↓than␈α∪the␈α∪heuristic␈α∀part␈α∪of␈α∪the␈α∀AI␈α∪problem.
␈↓ ↓:␈↓Another␈α∩phenomenon␈α∩that␈α∩shows␈α∩up␈α∪in␈α∩the           ␈↓ εz␈↓When␈α∪our␈α∪interest␈α∪turn␈α∪again␈α∀to␈α∪heuristics,
␈↓ ↓:␈↓chess␈α⊗problems␈α⊗and␈α⊗in␈α⊗common␈α⊗sense␈α∃real           ␈↓ εz␈↓chess␈α⊗may␈α⊗or␈α↔may␈α⊗not␈α⊗be␈α↔an␈α⊗appropriate
␈↓ ↓:␈↓world␈α'problems␈α(but␈α'not␈α(in␈α'ordinary               ␈↓ εz␈↓experimental domain.
␈↓ ↓:␈↓mattematics␈α6is␈α6parallel␈α6action,␈α5our
␈↓ ↓:␈↓understanding␈α⊃of␈α⊃its␈α⊂logic␈α⊃is␈α⊃still␈α⊂incomplete.   ␈↓ εz␈↓To␈α∃summarize␈α∀then,␈α∃the␈α∃Formal␈α∀Reasoning
␈↓ ↓:␈↓In␈α⊃chess,␈α∩the␈α⊃moves␈α∩of␈α⊃the␈α∩players␈α⊃alternate       ␈↓ εz␈↓Group␈α⊗is␈α↔involved␈α⊗in␈α↔a␈α⊗subproblem␈α↔of␈α⊗a
␈↓ ↓N␈↓α1.1  FORMAL REASONING␈↓ ←5


␈↓ ↓N␈↓subproblem␈α∩of␈α∪the␈α∩general␈α∩AI␈α∪problem,␈α∩but         ␈↓ π∞␈↓␈↓ π.within ≡rst order logic in a form usable in
␈↓ ↓N␈↓there␈α$is␈α#good␈α$reason␈α#to␈α$believe␈α#that              ␈↓ π∞␈↓␈↓ π.FOL.  This will permit us to use FOL for
␈↓ ↓N␈↓subproblems␈α∪can␈α∪be␈α∪solved␈α∪in␈α∪a␈α∪reasonable         ␈↓ π∞␈↓␈↓ π.the proofs about programs that have been
␈↓ ↓N␈↓time␈α⊂and␈α∂that␈α⊂their␈α∂solution␈α⊂will␈α⊂constitute␈α∂a     ␈↓ π∞␈↓␈↓ π.carried out in our specialized system LCF
␈↓ ↓N␈↓genuine␈αcontribution␈αto␈αthe␈αsolution␈αof␈α
the␈αAI     ␈↓ π∞␈↓␈↓ π.but with the greater power obtained by
␈↓ ↓N␈↓problem as a whole.                         ␈↓ π∞␈↓␈↓ π.including a full quanti≡er logic and set
                                            ␈↓ π∞␈↓␈↓ π.theory - by June 1975.
␈↓ ↓N␈↓α␈↓ α∞1.1.5  Goals and milestones.
                                            ␈↓ π∞␈↓3.  A major combinatorial theorem such as
␈↓ ↓N␈↓The␈α→Formal␈α→Reasoning␈α→Group␈α~intends␈α→to            ␈↓ π∞␈↓␈↓ π.Ramsey's theorem or van der Waerden's
␈↓ ↓N␈↓accomplish␈αthe␈αfollowing␈αspeci≡c␈αtasks␈α
between   ␈↓ π∞␈↓␈↓ π.theorem about arithmetic sequences in
␈↓ ↓N␈↓now␈α∂and␈α∂the␈α∂June␈α∂1977␈α∂as␈α∂well␈α∂as␈α∞obtaining          ␈↓ π∞␈↓␈↓ π.partitions of the integers will be proved
␈↓ ↓N␈↓presently␈α
unschedulable␈α
results.␈α Because␈α
many  ␈↓ π∞␈↓␈↓ π.within FOL.  This will con≡rm the
␈↓ ↓N␈↓of␈α∞them␈α
have␈α∞a␈α∞technical␈α
character,␈α∞it␈α∞will␈α
be      ␈↓ π∞␈↓␈↓ π.practicality of expressing the proofs of
␈↓ ↓N␈↓necessary␈α_to␈α_refer␈α→to␈α_the␈α_material␈α→of␈α_the          ␈↓ π∞␈↓␈↓ π.di≠cult mathematical theorems in FOL
␈↓ ↓N␈↓preceding␈αsection␈αin␈αorder␈αto␈αunderstand␈αtheir    ␈↓ π∞␈↓␈↓ π.with proofs of reasonable length and will
␈↓ ↓N␈↓cogency.                                    ␈↓ π∞␈↓␈↓ π.con≡rm that we really understand some of
                                            ␈↓ π∞␈↓␈↓ π.the major modes of reasoning that
␈↓ ↓N␈↓1.  Our proof-checker for ≡rst order logic  ␈↓ π∞␈↓␈↓ π.mathematicians actually use - by October
␈↓ ↓N␈↓␈↓ ↓ncalled FOL will be improved in the          ␈↓ π∞␈↓␈↓ π.1975.
␈↓ ↓N␈↓␈↓ ↓nfollowing ways:
                                            ␈↓ π∞␈↓4.  The reasoning involved in the two chess
␈↓ ↓N␈↓␈↓ ↓na.  The metamathematics of FOL              ␈↓ π∞␈↓␈↓ π.problems now being worked on will have
␈↓ ↓N␈↓␈↓ α∞expressions will be formalized, and         ␈↓ π∞␈↓␈↓ π.been expressed in a FOL form and
␈↓ ↓N␈↓␈↓ α∞syntactic functions realizing the abstract  ␈↓ π∞␈↓␈↓ π.checked.  The FOL proof will correspond
␈↓ ↓N␈↓␈↓ α∞syntax of FOL will be programmed and        ␈↓ π∞␈↓␈↓ π.closely in content and in length with the
␈↓ ↓N␈↓␈↓ α∞attached to the appropriate function        ␈↓ π∞␈↓␈↓ π.informal human argument.  This will
␈↓ ↓N␈↓␈↓ α∞symbols - by December 1975.                 ␈↓ π∞␈↓␈↓ π.con≡rm our understanding of the extensions
                                            ␈↓ π∞␈↓␈↓ π.to simple predicate calculus reasoning
␈↓ ↓N␈↓␈↓ ↓nb.  A powerful form of the re∨ection        ␈↓ π∞␈↓␈↓ π.required to express chess type reasoning -
␈↓ ↓N␈↓␈↓ α∞principle will be added with su≠cient       ␈↓ π∞␈↓␈↓ π.by September 1975.
␈↓ ↓N␈↓␈↓ α∞restrictions imposed to ensure that the
␈↓ ↓N␈↓␈↓ α∞extended logic is consistent - by January   ␈↓ π∞␈↓5.  A notion of abstract pattern that is a
␈↓ ↓N␈↓␈↓ α∞1976.                                       ␈↓ π∞␈↓␈↓ π.generalization of linguistic patterns will be
                                            ␈↓ π∞␈↓␈↓ π.further developed and applied to chess
␈↓ ↓N␈↓␈↓ ↓nc.  A facility for a user function to try to␈↓ π∞␈↓␈↓ π.temporal and spacial patterns.  This will
␈↓ ↓N␈↓␈↓ α∞generate a proof to be checked by FOL       ␈↓ π∞␈↓␈↓ π.develop our understanding of the patterns
␈↓ ↓N␈↓␈↓ α∞will be added - by June 1976.               ␈↓ π∞␈↓␈↓ π.used in human reasoning - by January
                                            ␈↓ π∞␈↓␈↓ π.1976.
␈↓ ↓N␈↓␈↓ ↓nd.  The newly added UNIFY and
␈↓ ↓N␈↓␈↓ α∞RESOLVE rules will be fully speci≡ed        ␈↓ π∞␈↓6.  Some concepts required to express what
␈↓ ↓N␈↓␈↓ α∞and their properties understood - by June   ␈↓ π∞␈↓␈↓ π.can be known about actions taken in
␈↓ ↓N␈↓␈↓ α∞1975.                                       ␈↓ π∞␈↓␈↓ π.parallel by di≥erent people will be put in
                                            ␈↓ π∞␈↓␈↓ π.FOL form - by June 1976.
␈↓ ↓N␈↓␈↓ ↓ne.  Goal structure like that in LCF will be
␈↓ ↓N␈↓␈↓ α∞added to FOL - by January 1976.             ␈↓ π∞␈↓7.  The results of Gordon's thesis will be
                                            ␈↓ π∞␈↓␈↓ π.extended to most of LISP 1.5 - by July
␈↓ ↓N␈↓2.  A form of Dana's Scott's logic of       ␈↓ π∞␈↓␈↓ π.1975. The modes of reasoning used to
␈↓ ↓N␈↓␈↓ ↓ncomputable functions will be axiomatized    ␈↓ π∞␈↓␈↓ π.obtain these results will be analysed and a
␈↓ ↓N␈↓α6␈↓ n


␈↓ ↓N␈↓␈↓ ↓nformalism for representing them developed   ␈↓ π∞␈↓problems.␈α≠ David␈α≠Wilkins␈α≠is␈α≤working␈α≠on
␈↓ ↓N␈↓␈↓ ↓n- by September 1975.  Embedding this        ␈↓ π∞␈↓generalized patterns with chess as an example.
␈↓ ↓N␈↓␈↓ ↓nformalism in FOL will be undertaken.

␈↓ ↓N␈↓8.  FOL will be used to express facts about
␈↓ ↓N␈↓␈↓ ↓nprojective geometry and about real world
␈↓ ↓N␈↓␈↓ ↓nscenes.  This will involve heavy use of the
␈↓ ↓N␈↓␈↓ ↓nfeature of FOL that allows attachment of
␈↓ ↓N␈↓␈↓ ↓nfunction symbols in the logic to machine
␈↓ ↓N␈↓␈↓ ↓nprograms - in this case even programs that
␈↓ ↓N␈↓␈↓ ↓nuse the TV camera - by June 1976.

␈↓ ↓N␈↓α␈↓ α∞1.1.6  The Formal Reasoning Group.

␈↓ ↓N␈↓John␈α↔McCarthy␈α_is␈α↔Professor␈α_of␈α↔Computer
␈↓ ↓N␈↓Science␈αand␈αhas␈αworked␈αin␈αthe␈αarea␈αof␈αformal
␈↓ ↓N␈↓reasoning␈α⊗applied␈α⊗to␈α⊗computer␈α⊗science␈α∃and
␈↓ ↓N␈↓arti≡cial␈α
intelligence␈α
since␈α
1957.␈α
 He␈α
is␈α
working
␈↓ ↓N␈↓on␈αthe␈αtranslation␈αof␈αthe␈αScott␈αtheory␈αin␈αFOL,
␈↓ ↓N␈↓on␈α
the␈α
expression␈α
of␈α
chess␈α
reasoning␈α
in␈αFOL,
␈↓ ↓N␈↓and␈α⊂on␈α⊂a␈α⊂formalism␈α⊂for␈α⊃generalized␈α⊂patterns
␈↓ ↓N␈↓again using ≡rst order logic.

␈↓ ↓N␈↓Richard␈α∂Weyhrauch␈α∂is␈α∂Research␈α∂Associate␈α∞in
␈↓ ↓N␈↓Computer␈α∞Science,␈α∞has␈α∞a␈α∞PhD␈α∂from␈α∞Stanford
␈↓ ↓N␈↓in␈α⊗mathematical␈α⊗logic␈α⊗and␈α⊗has␈α↔worked␈α⊗on
␈↓ ↓N␈↓mathematical␈α⊂theory␈α⊃of␈α⊂computation␈α⊃and␈α⊂the
␈↓ ↓N␈↓development␈α≠of␈α~proof-checkers.␈α≠ He␈α≠is␈α~in
␈↓ ↓N␈↓charge␈αof␈αthe␈αwork␈αon␈αFOL.␈α Bill␈αGlassmire␈α
is
␈↓ ↓N␈↓Research␈α∂Associate␈α⊂in␈α∂Computer␈α⊂Science,␈α∂has
␈↓ ↓N␈↓joined␈α⊂the␈α∂group␈α⊂recently,␈α∂is␈α⊂also␈α⊂a␈α∂Stanford
␈↓ ↓N␈↓PhD␈α∂in␈α∂mathematical␈α∂logic.␈α⊂ Weyhrauch␈α∂and
␈↓ ↓N␈↓Glassmire␈αare␈αextending␈αFOL␈αand␈αapplying␈αit
␈↓ ↓N␈↓to␈αproblems␈α
in␈αmathematics␈α
and␈αmathematical
␈↓ ↓N␈↓theory␈αof␈α
computation.␈α Michael␈α
Gordon␈αhas␈α
a
␈↓ ↓N␈↓PhD␈α
in␈α
computer␈α
science␈α
from␈α
the␈α
University
␈↓ ↓N␈↓of␈α∩Edinburgh.␈α⊃ His␈α∩thesis␈α⊃was␈α∩on␈α⊃reasoning
␈↓ ↓N␈↓about␈αa␈αsemantics␈αand␈αimplementation␈αof␈αpure
␈↓ ↓N␈↓LISP␈α↔within␈α↔the␈α↔Scott-Strachey␈α⊗framework.
␈↓ ↓N␈↓He␈α≠will␈α~pursue␈α≠the␈α~formalization␈α≠of␈α~the
␈↓ ↓N␈↓interactive␈α∪and␈α∀machine␈α∪oriented␈α∀aspects␈α∪of
␈↓ ↓N␈↓LISP.␈α∂ Arthur␈α∞Thomas␈α∂is␈α∞a␈α∂graduate␈α∞student
␈↓ ↓N␈↓in␈α∩psychology,␈α∩has␈α∪worked␈α∩on␈α∩FOL,␈α∪and␈α∩is
␈↓ ↓N␈↓interested␈α
in␈α
application␈α
of␈α
FOL␈α
to␈α
reasoning
␈↓ ↓N␈↓about␈α_projective␈α_geometry␈α_and␈α_to␈α_visually
␈↓ ↓N␈↓perceived␈α"scenes␈α"and␈α"other␈α#real␈α"world
␈↓ ↓N␈↓phenomena.␈α∃ Robert␈α⊗Filman␈α∃is␈α⊗working␈α∃on
␈↓ ↓N␈↓expressing␈α∪chess␈α∀reasoning␈α∪in␈α∀FOL.␈α∪ David
␈↓ ↓N␈↓Arnold␈α→is␈α→applying␈α→FOL␈α~to␈α→mathematical